Step of Proof: b2i_wf
9,38
postcript
pdf
Inference at
*
I
of proof for Lemma
b2i
wf
:
b
:
. b2i(
b
)
latex
by ((Unfold `b2i` 0)
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
C
)) (first_tok :t) inil_term)))
latex
C
.
Definitions
b2i(
b
)
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
bool
wf
,
ifthenelse
wf
origin